let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st B c= MaxADSet A & A c= MaxADSet B holds
MaxADSet A = MaxADSet B
let A, B be Subset of Y; :: thesis: ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B )
thus ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B ) :: thesis: verum

proof

assume that
A1: B c= MaxADSet A and
A2: A c= MaxADSet B ; :: thesis: MaxADSet A = MaxADSet B
A3: MaxADSet A c= MaxADSet B by A2, Th36;
MaxADSet B c= MaxADSet A by A1, Th36;
hence MaxADSet A = MaxADSet B by A3, XBOOLE_0:def 10; :: thesis: verum

end;