let x, y be Element of T; :: according to WAYBEL_0:def 20 :: thesis: ( not x in A ` or not x <= y or y in A ` )
assume that
A1: x in A ` and
A2: x <= y ; :: thesis: y in A `
not x in A by A1, XBOOLE_0:def 5;
then not y in A by A2, WAYBEL_0:def 19;
hence y in A ` by XBOOLE_0:def 5; :: thesis: verum