let X be set ; :: thesis: for SF being upper Subset-Family of X
for S being Element of SF holds meet SF c= S
let SF be upper Subset-Family of X; :: thesis: for S being Element of SF holds meet SF c= S
let S be Element of SF; :: thesis: meet SF c= S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet SF or x in S )
assume A1: x in meet SF ; :: thesis: x in S

per cases ( SF is empty or not SF is empty ) ;

suppose SF is empty ; :: thesis: x in S

hence x in S by A1, SETFAM_1:def 1; :: thesis: verum

end;

suppose not SF is empty ; :: thesis: x in S

hence x in S by A1, SETFAM_1:def 1; :: thesis: verum

end;

end;