[mazsa]

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

$)