let X be set ; :: thesis: for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds
rho (meet SF) c= SF
let SF be upper Subset-Family of [:X,X:]; :: thesis: ( meet SF in SF implies rho (meet SF) c= SF )
assume A1: meet SF in SF ; :: thesis: rho (meet SF) c= SF
thus rho (meet SF) c= SF :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rho (meet SF) or x in SF )
assume x in rho (meet SF) ; :: thesis: x in SF
then consider S being Subset of [:X,X:] such that
A2: x = S and
A3: meet SF c= S ;
SF is upper ;
hence x in SF by A2, A3, A1; :: thesis: verum
end;
thus verum ; :: thesis: verum