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

defpred S1[ Point of ()] means ( LE q1,\$1,P & LE \$1,q2,P );
{ p where p is Point of () : S1[p] } is Subset of () from then reconsider C = { p where p is Point of () : ( LE q1,p,P & LE p,q2,P ) } as Subset of () ;
( q2 <> W-min P implies C = { p where p is Point of () : ( LE q1,p,P & LE p,q2,P ) } ) ;
hence ex B being Subset of () st
( ( q2 <> W-min P implies B = { p where p is Point of () : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of () : ( 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 () st
( ( q2 <> W-min P implies B = { p where p is Point of () : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of () : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) )

defpred S1[ Point of ()] means ( LE q1,\$1,P or ( q1 in P & \$1 = W-min P ) );
{ p1 where p1 is Point of () : S1[p1] } is Subset of () from then reconsider C = { p1 where p1 is Point of () : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } as Subset of () ;
( not q2 <> W-min P implies C = { p1 where p1 is Point of () : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) ;
hence ex B being Subset of () st
( ( q2 <> W-min P implies B = { p where p is Point of () : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies B = { p1 where p1 is Point of () : ( 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 () : ( LE q1,p,P & LE p,q2,P ) } is Subset of () ) & ( not q2 <> W-min P implies { p1 where p1 is Point of () : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } is Subset of () ) & ( for b1 being Subset of () holds verum ) ) ; :: thesis: verum