let L be non empty transitive RelStr ; :: thesis: for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of
for Y being Subset of st X = Y holds
finsups X c= finsups Y
let S be non empty full sups-inheriting SubRelStr of L; :: thesis: for X being Subset of
for Y being Subset of st X = Y holds
finsups X c= finsups Y
let X be Subset of ; :: thesis: for Y being Subset of st X = Y holds
finsups X c= finsups Y
let Y be Subset of ; :: thesis: ( X = Y implies finsups X c= finsups Y )
assume A1: X = Y ; :: thesis: finsups X c= finsups Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups X or x in finsups Y )
assume x in finsups X ; :: thesis: x in finsups Y
then x in { ("\/" V,L) where V is finite Subset of : ex_sup_of V,L } by WAYBEL_0:def 27;
then consider Z being finite Subset of such that
A2: x = "\/" Z,L and
A3: ex_sup_of Z,L ;
reconsider Z = Z as finite Subset of by A1;
reconsider Z1 = Z as Subset of by XBOOLE_1:1;
A4: "\/" Z1,L in the carrier of S by A3, YELLOW_0:def 19;
then A5: ex_sup_of Z1,S by A3, YELLOW_0:65;
x = "\/" Z1,S by A2, A3, A4, YELLOW_0:65;
then x in { ("\/" V,S) where V is finite Subset of : ex_sup_of V,S } by A5;
hence x in finsups Y by WAYBEL_0:def 27; :: thesis: verum