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 set ; :: 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:37;
( y = "\/" Y,L & ex_sup_of {y},L ) by YELLOW_0:38, YELLOW_0:39;
hence x in finsups X ; :: thesis: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: verum

let x be set ; :: thesis: ( x in X implies x in fininfs X )
assume A2: 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 A2, ZFMISC_1:37;
( y = "/\" Y,L & ex_inf_of {y},L ) by YELLOW_0:38, YELLOW_0:39;
hence x in fininfs X ; :: thesis: verum

end;