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:
thus fininfs X c= finsups Y :: according to XBOOLE_0:def 10 :: thesis:
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:
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 ;
hence x in finsups Y by A1; :: thesis: verum
end;
thus finsups Y c= fininfs X :: thesis:
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:
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 ;
hence x in fininfs X by A1; :: thesis: verum
end;
thus finsups X c= fininfs Y :: according to XBOOLE_0:def 10 :: thesis:
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:
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 ;
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:
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 ;
hence x in finsups X by A1; :: thesis: verum