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
;
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 S1[
Point of
(TOP-REAL 2)]
means (
LE q1,$1,
P &
LE $1,
q2,
P );
{ p where p is Point of (TOP-REAL 2) : S1[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;
verum end; suppose A2:
not
q2 <> W-min P
;
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 S1[
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) : S1[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;
verum 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 b1 being Subset of (TOP-REAL 2) holds verum ) )
; verum