let A be Subset of L; :: thesis: (L,A,A)
let a be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( a in A implies ex b being Element of L st
( b in A & a <= b ) )
assume A1: a in A ; :: thesis: ex b being Element of L st
( b in A & a <= b )
take b = a; :: thesis: ( b in A & a <= b )
thus ( b in A & a <= b ) by A1; :: thesis: verum