let L be non empty reflexive antisymmetric RelStr ; :: thesis: for X being Subset of L holds
( X c= finsups X & X c= fininfs X )
let X be Subset of L; :: thesis: ( X c= finsups X & X c= fininfs X )

hereby :: according to TARSKI:def 3 :: thesis: X c= fininfs X

let x be object ; :: thesis: ( x in X implies x in finsups X )
assume A1: x in X ; :: thesis: x in finsups X
then reconsider y = x as Element of L ;
reconsider Y = {x} as finite Subset of X by A1, ZFMISC_1:31;
A2: y = "\/" (Y,L) by YELLOW_0:39;
ex_sup_of {y},L by YELLOW_0:38;
hence x in finsups X by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in fininfs X )
assume A3: x in X ; :: thesis: x in fininfs X
then reconsider y = x as Element of L ;
reconsider Y = {x} as finite Subset of X by A3, ZFMISC_1:31;
A4: y = "/\" (Y,L) by YELLOW_0:39;
ex_inf_of {y},L by YELLOW_0:38;
hence x in fininfs X by A4; :: thesis: verum