let L be non empty RelStr ; :: thesis: for X, Y being Subset of L st X c= Y holds

finsups X c= finsups Y

let X, Y be Subset of L; :: thesis: ( X c= Y implies finsups X c= finsups Y )

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

let x be object ; :: 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 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, XBOOLE_1:1;

ex_sup_of Z,L by A3;

then x in { ("\/" (V,L)) where V is finite Subset of Y : ex_sup_of V,L } by A2;

hence x in finsups Y by WAYBEL_0:def 27; :: thesis: verum

finsups X c= finsups Y

let X, Y be Subset of L; :: thesis: ( X c= Y implies finsups X c= finsups Y )

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

let x be object ; :: 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 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, XBOOLE_1:1;

ex_sup_of Z,L by A3;

then x in { ("\/" (V,L)) where V is finite Subset of Y : ex_sup_of V,L } by A2;

hence x in finsups Y by WAYBEL_0:def 27; :: thesis: verum