let L be non empty RelStr ; :: thesis: for X being Subset of L
for Y being Subset of (L opp) st X = Y holds
( fininfs X = finsups Y & finsups X = fininfs Y )
let X be Subset of L; :: thesis: for Y being Subset of (L opp) st X = Y holds
( fininfs X = finsups Y & finsups X = fininfs Y )
let Y be Subset of (L opp); :: thesis: ( X = Y implies ( fininfs X = finsups Y & finsups X = fininfs Y ) )
assume A1: X = Y ; :: thesis: ( fininfs X = finsups Y & finsups X = fininfs Y )
thus fininfs X c= finsups Y :: according to XBOOLE_0:def 10 :: thesis: ( finsups Y c= fininfs X & finsups X = fininfs Y )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in fininfs X or x in finsups Y )
assume x in fininfs X ; :: thesis: x in finsups Y
then consider Z being finite Subset of X such that
A2: ( x = "/\" (Z,L) & ex_inf_of Z,L ) ;
( x = "\/" (Z,(L opp)) & ex_sup_of Z,L opp ) by A2, Th11, Th13;
hence x in finsups Y by A1; :: thesis: verum

end;

thus finsups Y c= fininfs X :: thesis: finsups X = fininfs Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups Y or x in fininfs X )
assume x in finsups Y ; :: thesis: x in fininfs X
then consider Z being finite Subset of Y such that
A3: ( x = "\/" (Z,(L opp)) & ex_sup_of Z,L opp ) ;
( x = "/\" (Z,L) & ex_inf_of Z,L ) by A3, Th11, Th13;
hence x in fininfs X by A1; :: thesis: verum

end;

thus finsups X c= fininfs Y :: according to XBOOLE_0:def 10 :: thesis: fininfs Y c= finsups X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups X or x in fininfs Y )
assume x in finsups X ; :: thesis: x in fininfs Y
then consider Z being finite Subset of X such that
A4: ( x = "\/" (Z,L) & ex_sup_of Z,L ) ;
( x = "/\" (Z,(L opp)) & ex_inf_of Z,L opp ) by A4, Th10, Th12;
hence x in fininfs Y by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in fininfs Y or x in finsups X )
assume x in fininfs Y ; :: thesis: x in finsups X
then consider Z being finite Subset of Y such that
A5: ( x = "/\" (Z,(L opp)) & ex_inf_of Z,L opp ) ;
( x = "\/" (Z,L) & ex_sup_of Z,L ) by A5, Th10, Th12;
hence x in finsups X by A1; :: thesis: verum