let L be non empty transitive antisymmetric complete RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: for Y being Subset of S st X = Y holds

finsups X = finsups Y

let Y be Subset of S; :: thesis: ( X = Y implies finsups X = finsups Y )

assume A1: X = Y ; :: thesis: finsups X = finsups Y

hence finsups X c= finsups Y by Th3; :: according to XBOOLE_0:def 10 :: thesis: finsups Y c= finsups X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups Y or x in finsups X )

assume x in finsups Y ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: for Y being Subset of S st X = Y holds

finsups X = finsups Y

let Y be Subset of S; :: thesis: ( X = Y implies finsups X = finsups Y )

assume A1: X = Y ; :: thesis: finsups X = finsups Y

hence finsups X c= finsups Y by Th3; :: according to XBOOLE_0:def 10 :: thesis: finsups Y c= finsups X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups Y or x in finsups X )

assume x in finsups Y ; :: thesis: 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; :: thesis: verum