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 )

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

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

thus
finsups Y c= fininfs X
:: thesis: finsups X = fininfs Y
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;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

proof

thus
finsups X c= fininfs Y
:: according to XBOOLE_0:def 10 :: thesis: fininfs Y c= finsups X
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;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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in fininfs Y or x in finsups X )
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;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

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