let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in F "/\" F ; :: thesis:
then consider y, z being Element of L such that
A1: x = y "/\" z and
A2: ( y in F & z in F ) ;
consider t being Element of L such that
A3: t in F and
A4: ( t <= y & t <= z ) by A2, WAYBEL_0:def 2;
y "/\" z >= t by A4, YELLOW_0:23;
hence x in F by A1, A3, WAYBEL_0:def 20; :: thesis:

end;