I think you are right (metamath): $( <MM> <PROOF_ASST> THEOREM=whiteswans LOC_AFTER= * Assume it is provable that ( l e. S /\ l e. W ) implies for all l ( l e

I think you are right (metamath): $( <MM> <PROOF_ASST> THEOREM=whiteswans LOC_AFTER= * Assume it is provable that ( l e. S /\ l e. W ) implies for all l ( l e. S /\ l e. W ), and assume that g e. S . Then it is provable that if ( l e. S /\ l e. W ) then g e. W . h1::whiteswans.1 |- ( ( l e. S /\ l e. W ) -> A. l ( l e. S -> l e. W ) ) h2::whiteswans.2 |- g e. S 3:1:bnj1361 |- ( ( l e. S /\ l e. W ) -> S C_ W ) 5:3:sseld |- ( ( l e. S /\ l e. W ) -> ( g e. S -> g e. W ) ) qed:2,5:mpi |- ( ( l e. S /\ l e. W ) -> g e. W ) $= ( cv wcel wa bnj1361 sseld mpi ) DGZAHMCHIZBGZAHOCHFNACONDACEJKL $. $d S l $d W l $)