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 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 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