let L be non empty transitive antisymmetric complete 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 = 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 = finsups Y
let X be Subset of L; for Y being Subset of S st X = Y holds
finsups X = finsups Y
let Y be Subset of S; ( X = Y implies finsups X = finsups Y )
assume A1:
X = Y
; finsups X = finsups Y
hence
finsups X c= finsups Y
by Th3; XBOOLE_0:def 10 finsups Y c= finsups X
let x be object ; TARSKI:def 3 ( not x in finsups Y or x in finsups X )
assume
x in finsups Y
; x in finsups X
then
x in { ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S }
by WAYBEL_0:def 27;
then consider Z being finite Subset of Y such that
A2:
x = "\/" (Z,S)
and
ex_sup_of Z,S
;
reconsider Z = Z as finite Subset of X by A1;
reconsider Z1 = Z as Subset of S by XBOOLE_1:1;
A3:
ex_sup_of Z1,L
by YELLOW_0:17;
then
"\/" (Z1,L) in the carrier of S
by YELLOW_0:def 19;
then
x = "\/" (Z1,L)
by A2, A3, YELLOW_0:64;
then
x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L }
by A3;
hence
x in finsups X
by WAYBEL_0:def 27; verum