let L be non empty transitive RelStr ; for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let S be non empty full sups-inheriting SubRelStr of L; for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let X be Subset of L; for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let Y be Subset of S; ( X = Y implies finsups X c= finsups Y )
assume A1:
X = Y
; finsups X c= finsups Y
let x be object ; TARSKI:def 3 ( not x in finsups X or x in finsups Y )
assume
x in finsups X
; x in finsups Y
then
x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L }
by WAYBEL_0:def 27;
then consider Z being finite Subset of X such that
A2:
x = "\/" (Z,L)
and
A3:
ex_sup_of Z,L
;
reconsider Z = Z as finite Subset of Y by A1;
reconsider Z1 = Z as Subset of S 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:64;
x = "\/" (Z1,S)
by A2, A3, A4, YELLOW_0:64;
then
x in { ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S }
by A5;
hence
x in finsups Y
by WAYBEL_0:def 27; verum