set A = { [s,t] where s is Point of S, t is Point of T : s <> t } ;
{ [s,t] where s is Point of S, t is Point of T : s <> t } c= the carrier of [:S,T:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [s,t] where s is Point of S, t is Point of T : s <> t } or a in the carrier of [:S,T:] )
assume a in { [s,t] where s is Point of S, t is Point of T : s <> t } ; :: thesis: a in the carrier of [:S,T:]
then ex s being Point of S ex t being Point of T st
( a = [s,t] & s <> t ) ;
hence a in the carrier of [:S,T:] ; :: thesis: verum

end;

hence { [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:] ; :: thesis: verum