let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st (OSConstants OU0) \/ A is non-empty holds
OSMSubSort A is non-empty
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 st (OSConstants OU0) \/ A is non-empty holds
OSMSubSort A is non-empty
let A be OSSubset of OU0; :: thesis: ( (OSConstants OU0) \/ A is non-empty implies OSMSubSort A is non-empty )
assume A1: (OSConstants OU0) \/ A is non-empty ; :: thesis: OSMSubSort A is non-empty

now

let i be set ; :: thesis: ( i in the carrier of S1 implies not (OSMSubSort A) . i is empty )
assume i in the carrier of S1 ; :: thesis: not (OSMSubSort A) . i is empty
then reconsider s = i as SortSymbol of S1 ;
for Z being set st Z in OSSubSort A,s holds
((OSConstants OU0) \/ A) . s c= Z

proof

let Z be set ; :: thesis: ( Z in OSSubSort A,s implies ((OSConstants OU0) \/ A) . s c= Z )
assume Z in OSSubSort A,s ; :: thesis: ((OSConstants OU0) \/ A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
( OSConstants OU0 c= B & A c= B ) by A2, Th24;
then (OSConstants OU0) \/ A c= B by PBOOLE:18;
hence ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def 5; :: thesis: verum

end;

then A4: ((OSConstants OU0) \/ A) . s c= meet (OSSubSort A,s) by SETFAM_1:6;
ex x being set st x in ((OSConstants OU0) \/ A) . s by A1, XBOOLE_0:def 1;
hence not (OSMSubSort A) . i is empty by A4, Def11; :: thesis: verum

end;

hence OSMSubSort A is non-empty by PBOOLE:def 16; :: thesis: verum