let X be set ; :: thesis: for R being Relation of X holds
( rho R is upper & rho R is V288() )
let R be Relation of X; :: thesis: ( rho R is upper & rho R is V288() )
now :: thesis: for Y1, Y2 being Subset of [:X,X:] st Y1 in rho R & Y1 c= Y2 holds
Y2 in rho R
let Y1, Y2 be Subset of [:X,X:]; :: thesis: ( Y1 in rho R & Y1 c= Y2 implies Y2 in rho R )
assume that
A1: Y1 in rho R and
A2: Y1 c= Y2 ; :: thesis: Y2 in rho R
consider S being Subset of [:X,X:] such that
A3: Y1 = S and
A4: R c= S by A1;
R c= Y2 by A2, A3, A4;
hence Y2 in rho R ; :: thesis: verum
end;
hence rho R is upper ; :: thesis: rho R is V288()
now :: thesis: for X1, Y1 being set st X1 in rho R & Y1 in rho R holds
X1 /\ Y1 in rho R
let X1, Y1 be set ; :: thesis: ( X1 in rho R & Y1 in rho R implies X1 /\ Y1 in rho R )
assume that
A5: X1 in rho R and
A6: Y1 in rho R ; :: thesis: X1 /\ Y1 in rho R
consider SX being Subset of [:X,X:] such that
A7: X1 = SX and
A8: R c= SX by A5;
consider SY being Subset of [:X,X:] such that
A9: Y1 = SY and
A10: R c= SY by A6;
R c= SX /\ SY by A8, A10, XBOOLE_1:19;
hence X1 /\ Y1 in rho R by A7, A9; :: thesis: verum
end;
hence rho R is V288() ; :: thesis: verum