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 ) ) } ) )_{1} being Subset of (TOP-REAL 2) holds verum ) )
; :: thesis: verum

( ( 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
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 bper cases
( q2 <> W-min P or not q2 <> W-min P )
;

end;

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 ) ) } ) )

( ( 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_{1}[ Point of (TOP-REAL 2)] means ( LE q1,$1,P & LE $1,q2,P );

{ p where p is Point of (TOP-REAL 2) : S_{1}[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;{ p where p is Point of (TOP-REAL 2) : S

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

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 ) ) } ) )

( ( 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_{1}[ 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_{1}[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;{ p1 where p1 is Point of (TOP-REAL 2) : S

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