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