meet { (x . O) where x is Element of X : x in L } c= X

proof

hence
meet { (x . O) where x is Element of X : x in L } is List of X
; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in meet { (x . O) where x is Element of X : x in L } or z in X )

assume A4: z in meet { (x . O) where x is Element of X : x in L } ; :: thesis: z in X

then { (x . O) where x is Element of X : x in L } <> {} by SETFAM_1:def 1;

then consider Y being object such that

A5: Y in { (x . O) where x is Element of X : x in L } by XBOOLE_0:def 1;

consider x being Element of X such that

A6: ( Y = x . O & x in L ) by A5;

z in x . O by A4, A5, A6, SETFAM_1:def 1;

hence z in X ; :: thesis: verum

end;assume A4: z in meet { (x . O) where x is Element of X : x in L } ; :: thesis: z in X

then { (x . O) where x is Element of X : x in L } <> {} by SETFAM_1:def 1;

then consider Y being object such that

A5: Y in { (x . O) where x is Element of X : x in L } by XBOOLE_0:def 1;

consider x being Element of X such that

A6: ( Y = x . O & x in L ) by A5;

z in x . O by A4, A5, A6, SETFAM_1:def 1;

hence z in X ; :: thesis: verum