ex B being Subset of (TOP-REAL 2) st
( ( q2 <> W-min P implies B = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) )

proof

per cases ( q2 <> W-min P or not q2 <> W-min P ) ;

suppose A1: q2 <> W-min P ; :: thesis: ex B being Subset of (TOP-REAL 2) st
( ( q2 <> W-min P implies B = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) )

defpred S₁[ Point of (TOP-REAL 2)] means ( LE q1,$1,P & LE $1,q2,P );
{ p where p is Point of (TOP-REAL 2) : S₁[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider C = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } as Subset of (TOP-REAL 2) ;
( q2 <> W-min P implies C = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) ;
hence ex B being Subset of (TOP-REAL 2) st
( ( q2 <> W-min P implies B = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) ) by A1; :: thesis: verum

end;

suppose A2: not q2 <> W-min P ; :: thesis: ex B being Subset of (TOP-REAL 2) st
( ( q2 <> W-min P implies B = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) )

defpred S₁[ Point of (TOP-REAL 2)] means ( LE q1,$1,P or ( q1 in P & $1 = W-min P ) );
{ p1 where p1 is Point of (TOP-REAL 2) : S₁[p1] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider C = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } as Subset of (TOP-REAL 2) ;
( not q2 <> W-min P implies C = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) ;
hence ex B being Subset of (TOP-REAL 2) st
( ( q2 <> W-min P implies B = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) ) by A2; :: thesis: verum

end;

end;

end;

hence ( ( q2 <> W-min P implies { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } is Subset of (TOP-REAL 2) ) & ( not q2 <> W-min P implies { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } is Subset of (TOP-REAL 2) ) & ( for b₁ being Subset of (TOP-REAL 2) holds verum ) ) ; :: thesis: verum