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 )

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

( 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in 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;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

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